$M$.init($x$,$v$) \\[0ex]$\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$fpf{-}val(IdDeq; 1of(2of(2of($M$))); $x$; $a$,$x_{0}$.($v$ $=$ $x_{0}$ $\in$ fpf{-}cap(1of($M$);IdDeq;$x$;Void)))